$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), $a$:$T$, $L$:($T$ List). insert(${\it eq}$; $a$; $L$) $\in$ ($T$ List)